es:event_system{i:l}, x,i:Id, T:Type, c:T.
(x,y:T. decidable((x = y  T)))
 es-dtype(es; i; x; T)
 (e:es-E(es). (loc(e) = i)  (es-first(es; e))  (es-when(es; x; e) = c))
 (e':es-E(es). 
 (loc(e') = i)
  ((es-after(es; x; e') = c))
  (ev:es-E(es). (es-le(es; ev; e')  ((es-after(es; x; ev) = es-when(es; x; ev)  T))))) 

latex

Definitions	guard(T), sq_type(T), A c B, P  Q, x:A. B(x), prop{i:l}, t  T, P  Q, x:A. B(x), es-dtype(es; i; x; T)
Lemmas	Id sq, es-le wf, change-lemma, es-le-loc, event system wf, Id wf, decidable wf, es-dtype wf, es-when wf, es-vartype wf, es-after wf, not wf, es-first-exists